f:(). (n:. f(n))  {f(mu(f)) & (i:. i<mu(f)  f(i))} 

latex

Definitions	T, True, Dec(P), P  Q, SQType(T), ij, Unit, P  Q, False, Prop, b, t  T, , x:A. B(x), AB, {T}, P & Q, x:A. B(x), , P  Q, mu(f), A, b
Lemmas	assert wf, not wf, bnot wf, bool wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, le wf, nat wf, nat properties, ge wf, decidable int equal, true wf, squash wf, mu wf